Fix #7807: Add case for MatchTypes to ApproximatingTypeMap #7835
Conversation
|
They are mostly boring fixes to fuzzing errors. If someone wants to review, please go ahead. But I feel we should not spend anymore time than necessary on this. |
| @@ -0,0 +1,3 @@ | |||
| object Test with | |||
|
|
|||
| def flip: (x: 0 | 1) => x.type match { case 0 => 1 case 1 => 0 } = ??? | |||
There was a problem hiding this comment.
I would add some more tests:
flip(0): 1
flip(1): 0
flip(if ??? then 0 else 1)
val n: 0 | 1 = if ??? then 0 else 1
flip(n)
val m: n.type match { case 0 => 1 case 1 => 0 } = flip(n)But I noticed a strange thing: a match type is apparently not a subtype of the union of it branches. So adding flip(m) or flip(flip(n)) for instance does not work:
-- [E007] Type Mismatch Error: tests/pos/i7807.scala:15:8 --------------------------------------------------------------
15 | flip(m)
| ^
| Found: (Test.m :
| (Test.n : (0 : Int) | (1 : Int)) match {
| case (0 : Int) => (1 : Int)
| case (1 : Int) => (0 : Int)
| }
| )
| Required: (0 : Int) | (1 : Int)Should an issue be opened about this? Though it seems the current spec does not say this should work, I find it surprising that it does not.
There was a problem hiding this comment.
I am not sure it should work. Generally, match types are on a thin line between expressiveness and soundness. So generally demanding they do more than they do would have to come with an algorithm that shows how to do it and an argument why this would not break soundness.
There was a problem hiding this comment.
Here are some more problems I found while playing with match types on the branch of this fix:
object Test2 with
type Flip[N <: 0 | 1] <: 0 | 1 = N match { case 0 => 1 case 1 => 0 }
def flip: (x: 0 | 1) => Flip[x.type] = ???
flip(0): 1 // ! does not type check
flip(1): 0
object Test3 with
type Flip[N <: 0 | 1] <: 0 | 1 = N match { case 0 => 1 case 1 => 0 }
def flip(x: 0 | 1): Flip[x.type] = ???
flip(0): 1 // ! causes: pickling difference for module class Test2$ in tests/pos/i7807.scala
flip(1): 0
flip(if ??? then 0 else 1)
val n: 0 | 1 = if ??? then 0 else 1
flip(n)
flip(flip(n)) // ! does not type check
|
I fixed the original issue but do not have time to pursue this topic further. @LPTK can you open new issues and assign to @OlivierBlanvillain? Thanks! |
There was a problem hiding this comment.
Okay, I have opened a new issue for the other crashes here: #7872
And an issue for the subtype-of-union problem here: https://github.com/lampepfl/dotty/issues/7873
Thanks to Lionel.
No description provided.